{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators,
  UndecidableInstances, ScopedTypeVariables #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module CnvExample where

import TypeBasics
import Yoko



data Exp = Const Int | Plus Exp Exp



data Fds_Const = Fds_Const Int
data Fds_Plus  = Fds_Plus  Exp Exp
type instance Tag Fds_Const = TagConst   ;   data TagConst
type instance Tag Fds_Plus  = TagPlus    ;   data TagPlus
type instance Range Fds_Const = Exp
type instance Range Fds_Plus  = Exp
instance DC Fds_Const where rejoin (Fds_Const i)     = Const i
instance DC Fds_Plus  where rejoin (Fds_Plus  el er) = Plus  el er
type instance DCs Exp = N Fds_Const :+ N Fds_Plus
instance DT Exp where
  disband (Const i)     = DCsOf $ Le . N $ Fds_Const  i
  disband (Plus  el er) = DCsOf $ Ri . N $ Fds_Plus   el er
type instance Rep Fds_Const = D Int
type instance Rep Fds_Plus  = R Exp :* R Exp
instance Generic Fds_Const where
  rep ~(Fds_Const i) = D i
  obj ~(D i)         = Fds_Const i
instance Generic Fds_Plus where
  rep ~(Fds_Plus el er) = R el :* R er
  obj ~(R el :* R er) = Fds_Plus el er





data Exp2 = Const2 Int (Maybe Exp2) | Plus2 Exp2 Exp2 deriving Show



data Fds_Const2 = Fds_Const2 Int (Maybe Exp2)
data Fds_Plus2  = Fds_Plus2  Exp2 Exp2
type instance Tag Fds_Const2 = TagConst2   ;   data TagConst2
type instance Tag Fds_Plus2  = TagPlus2    ;   data TagPlus2
type instance Range Fds_Const2 = Exp2
type instance Range Fds_Plus2  = Exp2
instance DC Fds_Const2 where rejoin (Fds_Const2 i me)     = Const2 i me
instance DC Fds_Plus2  where rejoin (Fds_Plus2  el er) = Plus2  el er
type instance DCs Exp2 = N Fds_Const2 :+ N Fds_Plus2
instance DT Exp2 where
  disband (Const2 i me)  = DCsOf $ Le . N $ Fds_Const2 i me
  disband (Plus2  el er) = DCsOf $ Ri . N $ Fds_Plus2  el er
type instance Rep Fds_Const2 = D Int :* Maybe (R Exp2)
type instance Rep Fds_Plus2  = R Exp2 :* R Exp2
instance Generic Fds_Const2 where
  rep ~(Fds_Const2 i me) = D i :* fmap R me
  obj ~(D i :* me)       = Fds_Const2 i (fmap unR me)
instance Generic Fds_Plus2 where
  rep ~(Fds_Plus2 el er) = R el :* R er
  obj ~(R el :* R er) = Fds_Plus2 el er











type instance IsPrefixOf TagConst TagConst2 = True
type instance IsPrefixOf TagConst TagPlus2  = False
type instance IsPrefixOf TagPlus  TagConst2 = False
type instance IsPrefixOf TagPlus  TagPlus2  = True









-- detail not in paper by the time this example is discussed
instance ToExp2 sum => ToExp2 (DCsOf t sum) where
  convert2 = convert2 . unDCsOf





class ToExp2 a where convert2 :: a -> Exp2

instance ToExp2 Exp where
  convert2 e = case project (disband e) of
    Left  (Fds_Const i) -> Const2 i Nothing
    Right x             -> convert2 x

{- ill-typed:     "Couldn't match type `Maybe (R Exp2)' with `Int'"
              and "Couldn't match type `(:*) (D Int)' with `D'"
              because the fields of Const and Const2 are inequal
   convert2 = convert2 . disband -}





instance (ToExp2 a, ToExp2 b) => ToExp2 (a :+ b) where
  convert2 = foldPlus convert2 convert2

-- NB only works if there's exactly one matching constructor
instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs Exp2),
          ToExp2Rs (Rep dc), Rep dc' ~ RsToExp2 (Rep dc),
          DC dc', Range dc' ~ Exp2
         ) => ToExp2 (N dc) where
  convert2 = foldN $ rejoin . (id :: dc' -> dc') . obj . convertRs2 . rep



type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (IsPrefixOf s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+ b) = DistMaybePlus (FindDCs s a) (FindDCs s b)




-- applies ToExp2 to every R in a product; identity on other factors
type family RsToExp2 prod
class ToExp2Rs prod where convertRs2 :: prod -> RsToExp2 prod

type instance RsToExp2 (R a) = R Exp2
instance ToExp2 a => ToExp2Rs (R a) where
  convertRs2 (R x) = R (convert2 x)

type instance RsToExp2 (D a) = D a
type instance RsToExp2 U     = U
instance ToExp2Rs (D a) where convertRs2 = id
instance ToExp2Rs U     where convertRs2 = id

type instance RsToExp2 (a :* b) = RsToExp2 a :* RsToExp2 b
instance (ToExp2Rs a, ToExp2Rs b) => ToExp2Rs (a :* b) where
  convertRs2 = mapTimes convertRs2 convertRs2



ex0 = convert2 (Plus (Const 3) (Const 4))




concat `fmap` mapM derive [''Fds_Const, ''Fds_Plus, ''Exp,
                           ''Fds_Const2, ''Fds_Plus2, ''Exp2]
